Nuprl Lemma : rps_wf
0,22
postcript
pdf
x
,
y
:
3. rps(
x
;
y
)
latex
Definitions
rps(
x
;
y
)
,
p
q
,
p
q
,
i
=
j
,
x
:
A
B
(
x
)
,
{
x
:
A
|
B
(
x
) }
,
{
i
..
j
}
,
x
:
A
.
B
(
x
)
,
t
T
,
#$n
Lemmas
int
seg
wf
,
eq
int
wf
,
band
wf
,
bor
wf
origin
x, y:
3. rps(x;y) 
x, y:3. rps(x;y) 
q
qj
B(x)
}x:A. B(x) T